Library reflection

Require Import PointsETC.
Require Import midpoint.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition reflection U P :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
   cTriple ((a×p-b×q-c×r)*u+2×p*(b×v+c×w))
          ((b×q-a×p-c×r)*v+2×q*(a×u+c×w))
          ((c×r-a×p-b×q)*w+2×r*(a×u+b×v))
 end.

Lemma X1_is_reflection_of_X8_X10 :
 eq_points X_1 (reflection X_8 X_10).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.

Lemma reflection_midpoint : ∀ A B,
 eq_points (midpoint A (reflection A B)) B.
Proof.
intros.
destruct A.
destruct B.
simpl.
unfold eq_points;simpl.
repeat split;ring.
Qed.

End Triangle.